Nuprl Lemma : mon_hom_inj_p_wf
13,42
postcript
pdf
g
,
h
:GrpSig,
f
:(|
g
|
|
h
|). IsMonHomInj(
g
;
h
;
f
)
latex
Up
groups
1
Definitions of Statement
IsMonHomInj(
g
;
h
;
f
)
Definitions
P
&
Q
,
IsMonHomInj(
g
;
h
;
f
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
grp
sig
wf
,
grp
car
wf
,
inject
wf
,
monoid
hom
p
wf
origin
g, h:GrpSig, f:(|g|
|h|). IsMonHomInj(g;h;f) 
g, h:GrpSig, f:(|g||h|). IsMonHomInj(g;h;f) Tx:A. B(x)